鹿島 亮; "コンピュータサイエンスにおける様相論理"
メモ
この本では次の論理を扱う
および
様相μ計算（便宜上$ \bold{C}_\muと表す） 論理$ \mathscr{L}
論理$ \mathscr{L}の証明体系$ \mathcal{H}_\mathscr{L}（Hilbert流演繹体系による） 論理$ \mathscr{L}の論理式$ \varphiについて
1. $ \varphiが論理$ \mathscr{L}において恒真
2. $ \varphiは$ \mathcal{H}_\mathscr{L}で証明可能
様相論理$ \mathscr{L} = \bold{K},\bold{CTL},\bold{CTL*},\bold{C}_\mu,\bold{PDF}のKripkeモデルについて Kripkeモデル$ K = \lang S, \rightsquigarrow, f\rangとしたとき 任意の論理式$ \varphiについて次は同値である
$ \varphiが$ \mathscr{L}恒真ではない
$ \varphiを偽とするようなあるモデル$ Mおよびそのモデルのある状態$ sが存在する
次のことが同値
$ \varphiが$ \mathscr{L}恒真でない
状態数が$ g({Lh}(\varphi))（ただし$ gは計算可能関数、$ g(x) = 2^xとか）以下のあるモデル$ Mおよびその状態$ sで$ \varphiが偽
論理式$ \varphiが恒真でないことは次と同値である
状態数が$ 2^{Lh(\varphi)}以下の有限Kripkeモデルのある状態で偽となるようなモデルが存在する 正規様相論理Kの論理式の集合$ \Gammaについて（有限，無限問わず） $ \Gammaの$ \bold{K}充足可能
$ \Gammaの全ての要素$ \gammaについて$ M,s \models \gammaを満たすような$ Mおよび$ Mの状態$ sが存在するとき
$ \Gammaが$ \mathcal{H}_\bold{K}矛盾
$ \Gammaの有限個の$ \gamma_1 \cdots \gamma_n，$ 1 \leq nについて
$ \mathcal{H}_\bold{K} \vdash \lnot( \gamma_1 \land \cdots \land \gamma_n)
$ \Gammaが$ \mathcal{H}_\bold{K}無矛盾
$ \Gammaが$ \mathcal{H}_\bold{K}矛盾ではない
$ \Gammaが極大$ \mathcal{H}_\bold{K}無矛盾
$ \mathcal{H}_\bold{K}無矛盾かつ
任意の論理式$ \varphiについて$ \varphi \in \Gammaか$ \lnot \varphi \in \Gamma
省略
定理1
任意の論理式集合について次のことは同値
1. $ \Gammaが$ \mathcal{H}_\bold{K}無矛盾
2. $ \Gammaが$ \bold{K}充足可能
証明
2→1: 対偶を示す
1→2: カノニカルモデルが$ \Gammaを充足することを示せば良いらしい（SnO2WMaN.iconなんで？）
$ \bold{K}の完全性の証明
任意の$ \bold{K}論理式$ \varphiについて
$ \varphiが$ \bold{K}恒真なら$ \mathcal{H}_\bold{K} \vdash \varphi
対偶を示す
$ \mathcal{H}_\bold{K} \not\vdash \varphiなら$ \varphiが$ \bold{K}恒真ではない
$ \mathcal{H}_\bold{K} \not\vdash \varphiから$ \{ \lnot \varphi \}は$ \mathcal{H}_\bold{K}無矛盾
仮に$ \{\lnot \varphi\}が$ \mathcal{H}_\bold{K}矛盾だった場合$ \lnot\lnot\varphi = \varphiとなって前提と矛盾する
よって$ \{ \lnot \varphi \}は$ \bold{K}充足可能
定理1より
よって$ \lnot \varphiは$ \bold{K}充足可能
論理式集合に関しての充足の定義より
よって$ M,s \models \lnot \varphi \iff M,s \not\models \varphiとなるようなモデル$ Mとその状態$ sが存在することを示された
$ \bold{K}の意味論の定義より
つまり$ \varphiは$ \bold{K}恒真ではない
恒真の定義より